;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(interface iGreyscale
  (sig greyscale (tree))
  (sig make-greyscale-columns (row columns))
  (sig pixel-to-greyscale (col r g b))
  
  ; pixel-to-greyscale returns a list of 4 numbers:
  ; the column number followed by three numbers between [0, 255]
  (con pixel-to-greyscale-returns-list-of-4
       (implies (and (and (natp r) (<= r 255))
                     (and (natp g) (<= g 255))
                     (and (natp b) (<= b 255))
                     (natp col))
                (let* ((newRGB (pixel-to-greyscale col r g b))
                       (newR   (cadr rgb))
                       (newG   (caddr rgb))
                       (newB   (cadddr rgb)))
                  (and (= (len newRGB) 4)
                       (and (natp newR) (<= newR 255))
                       (and (natp newG) (<= newG 255))
                       (and (natp newB) (<= newB 255))))))
  
  ; pixel-to-greyscale returns a grey value,
  ; meaning r = g = b.
  (con pixel-to-greyscale-works
       (implies (and (and (natp r) (<= r 255))
                     (and (natp g) (<= g 255))
                     (and (natp b) (<= b 255))
                     (natp col))
                (let* ((grey (pixel-to-greyscale col r g b ))
                       (newR (cadr grey))
                       (newG (caddr grey))
                       (newB (cadddr grey)))
                  (and (equal newR newG)
                       (equal newG newB)))))
  
  ; The greyscale function returns a tree.
  (con greyscale-returns-tree
       (implies (bmptree? tr)
                (bmptree? (greyscale tr)))))
